D:Dsys, i:Id, s:M(i).(timed)state, k:Knd, v:d-decl(D;i)(k).
Feasible(D)  (next-world-state(D;i;s;k;v)  d-world-state(D;i)) 

latex

Definitions	x:A. B(x), P  Q, t  T, d-world-state(D;i), next-world-state(D;i;s;k;v), Feasible(D), P & Q, , P  Q
Lemmas	d-decl-subtype, IdLnk wf, filter type, ma-msg wf, eq id wf, lsrc wf, mlnk wf d, ma-send-val wf, read-state wf, doact wf, d-feasible wf, d-decl wf, Knd wf, ma-tst wf, d-m wf, Id wf, dsys wf, subtype rel list, assert wf, assert-eq-id